InforLorV4, Main, Exploration, bibRecord, 004465

A Logical Account of PSPACE

Identifieur interne : 004465 ( Main/Exploration ); précédent : 004464; suivant : 004466

A Logical Account of PSPACE

Auteurs : Marco Gaboardi [Italie] ; Simona Ronchi Della Rocca [Italie] ; Jean-Yves Marion [France]

Source :

ACM SIGPLAN notices [ 1523-2867 ] ; 2008.

RBID : Pascal:08-0215615

Descripteurs français

Pascal (Inist)
- Langage programmation, Lambda calcul, Logique linéaire, Temps polynomial, Machine Turing, Complexité calcul, Logique booléenne, ..
Wicri :
- topic : Langage de programmation.

English descriptors

KwdEn :
- Boolean logic, Computational complexity, Lambda calculus, Linear logic, Polynomial time, Programming language, Turing machine.

Abstract

We propose a characterization of PSPACE by means of a type assignment for an extension of lambda calculus with a conditional construction. The type assignment STAB is an extension of STA, a type assignment for lambda-calculus inspired by Lafont's Soft Linear Logic. We extend STA by means of a ground type and terms for booleans. The key point is that the elimination rule for booleans is managed in an additive way. Thus, we are able to program polynomial time Alternating Turing Machines. Conversely, we introduce a call-by-name evaluation machine in order to compute programs in polynomial space. As far as we know, this is the first characterization of PSPACE which is based on lambda calculus and light logics.

Affiliations:

Links toward previous steps (curation, corpus...)

to stream PascalFrancis, to step Corpus: 000316
to stream PascalFrancis, to step Curation: 000711
to stream PascalFrancis, to step Checkpoint: 000285
to stream Main, to step Merge: 004580
to stream Main, to step Curation: 004465

Le document en format XML

<record><TEI><teiHeader><fileDesc><titleStmt><title xml:lang="en" level="a">A Logical Account of PSPACE</title>
<author><name sortKey="Gaboardi, Marco" sort="Gaboardi, Marco" uniqKey="Gaboardi M" first="Marco" last="Gaboardi">Marco Gaboardi</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Dipartimento di Informatica, Università degli Studi di Torino -Corso Svizzera 185</s1>
<s2>10149 Torino</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<placeName><settlement type="city">Turin</settlement>
<region type="région" nuts="2">Piémont</region>
</placeName>
</affiliation>
</author>
<author><name sortKey="Della Rocca, Simona Ronchi" sort="Della Rocca, Simona Ronchi" uniqKey="Della Rocca S" first="Simona Ronchi" last="Della Rocca">Simona Ronchi Della Rocca</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Dipartimento di Informatica, Università degli Studi di Torino -Corso Svizzera 185</s1>
<s2>10149 Torino</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<placeName><settlement type="city">Turin</settlement>
<region type="région" nuts="2">Piémont</region>
</placeName>
</affiliation>
</author>
<author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name>
<affiliation wicri:level="3"><inist:fA14 i1="02"><s1>Nancy-University, ENSMN-INPL, Loria B.P. 239</s1>
<s2>54506 Vandoeuvre-les-Nancy</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
</affiliation>
</author>
</titleStmt>
<publicationStmt><idno type="wicri:source">INIST</idno>
<idno type="inist">08-0215615</idno>
<date when="2008">2008</date>
<idno type="stanalyst">PASCAL 08-0215615 INIST</idno>
<idno type="RBID">Pascal:08-0215615</idno>
<idno type="wicri:Area/PascalFrancis/Corpus">000316</idno>
<idno type="wicri:Area/PascalFrancis/Curation">000711</idno>
<idno type="wicri:Area/PascalFrancis/Checkpoint">000285</idno>
<idno type="wicri:explorRef" wicri:stream="PascalFrancis" wicri:step="Checkpoint">000285</idno>
<idno type="wicri:doubleKey">1523-2867:2008:Gaboardi M:a:logical:account</idno>
<idno type="wicri:Area/Main/Merge">004580</idno>
<idno type="wicri:Area/Main/Curation">004465</idno>
<idno type="wicri:Area/Main/Exploration">004465</idno>
</publicationStmt>
<sourceDesc><biblStruct><analytic><title xml:lang="en" level="a">A Logical Account of PSPACE</title>
<author><name sortKey="Gaboardi, Marco" sort="Gaboardi, Marco" uniqKey="Gaboardi M" first="Marco" last="Gaboardi">Marco Gaboardi</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Dipartimento di Informatica, Università degli Studi di Torino -Corso Svizzera 185</s1>
<s2>10149 Torino</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<placeName><settlement type="city">Turin</settlement>
<region type="région" nuts="2">Piémont</region>
</placeName>
</affiliation>
</author>
<author><name sortKey="Della Rocca, Simona Ronchi" sort="Della Rocca, Simona Ronchi" uniqKey="Della Rocca S" first="Simona Ronchi" last="Della Rocca">Simona Ronchi Della Rocca</name>
<affiliation wicri:level="1"><inist:fA14 i1="01"><s1>Dipartimento di Informatica, Università degli Studi di Torino -Corso Svizzera 185</s1>
<s2>10149 Torino</s2>
<s3>ITA</s3>
<sZ>1 aut.</sZ>
<sZ>2 aut.</sZ>
</inist:fA14>
<country>Italie</country>
<placeName><settlement type="city">Turin</settlement>
<region type="région" nuts="2">Piémont</region>
</placeName>
</affiliation>
</author>
<author><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name>
<affiliation wicri:level="3"><inist:fA14 i1="02"><s1>Nancy-University, ENSMN-INPL, Loria B.P. 239</s1>
<s2>54506 Vandoeuvre-les-Nancy</s2>
<s3>FRA</s3>
<sZ>3 aut.</sZ>
</inist:fA14>
<country>France</country>
<placeName><region type="region" nuts="2">Grand Est</region>
<region type="old region" nuts="2">Lorraine (région)</region>
<settlement type="city">Vandœuvre-lès-Nancy</settlement>
</placeName>
</affiliation>
</author>
</analytic>
<series><title level="j" type="main">ACM SIGPLAN notices</title>
<title level="j" type="abbreviated">ACM SIGPLAN not.</title>
<idno type="ISSN">1523-2867</idno>
<imprint><date when="2008">2008</date>
</imprint>
</series>
</biblStruct>
</sourceDesc>
<seriesStmt><title level="j" type="main">ACM SIGPLAN notices</title>
<title level="j" type="abbreviated">ACM SIGPLAN not.</title>
<idno type="ISSN">1523-2867</idno>
</seriesStmt>
</fileDesc>
<profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Boolean logic</term>
<term>Computational complexity</term>
<term>Lambda calculus</term>
<term>Linear logic</term>
<term>Polynomial time</term>
<term>Programming language</term>
<term>Turing machine</term>
</keywords>
<keywords scheme="Pascal" xml:lang="fr"><term>Langage programmation</term>
<term>Lambda calcul</term>
<term>Logique linéaire</term>
<term>Temps polynomial</term>
<term>Machine Turing</term>
<term>Complexité calcul</term>
<term>Logique booléenne</term>
<term>.</term>
</keywords>
<keywords scheme="Wicri" type="topic" xml:lang="fr"><term>Langage de programmation</term>
</keywords>
</textClass>
</profileDesc>
</teiHeader>
<front><div type="abstract" xml:lang="en">We propose a characterization of PSPACE by means of a type assignment for an extension of lambda calculus with a conditional construction. The type assignment STAB is an extension of STA, a type assignment for lambda-calculus inspired by Lafont's Soft Linear Logic. We extend STA by means of a ground type and terms for booleans. The key point is that the elimination rule for booleans is managed in an additive way. Thus, we are able to program polynomial time Alternating Turing Machines. Conversely, we introduce a call-by-name evaluation machine in order to compute programs in polynomial space. As far as we know, this is the first characterization of PSPACE which is based on lambda calculus and light logics.</div>
</front>
</TEI>
<affiliations><list><country><li>France</li>
<li>Italie</li>
</country>
<region><li>Grand Est</li>
<li>Lorraine (région)</li>
<li>Piémont</li>
</region>
<settlement><li>Turin</li>
<li>Vandœuvre-lès-Nancy</li>
</settlement>
</list>
<tree><country name="Italie"><region name="Piémont"><name sortKey="Gaboardi, Marco" sort="Gaboardi, Marco" uniqKey="Gaboardi M" first="Marco" last="Gaboardi">Marco Gaboardi</name>
</region>
<name sortKey="Della Rocca, Simona Ronchi" sort="Della Rocca, Simona Ronchi" uniqKey="Della Rocca S" first="Simona Ronchi" last="Della Rocca">Simona Ronchi Della Rocca</name>
</country>
<country name="France"><region name="Grand Est"><name sortKey="Marion, Jean Yves" sort="Marion, Jean Yves" uniqKey="Marion J" first="Jean-Yves" last="Marion">Jean-Yves Marion</name>
</region>
</country>
</tree>
</affiliations>
</record>

Pour manipuler ce document sous Unix (Dilib)

EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration

HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 004465 | SxmlIndent | more

HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 004465 | SxmlIndent | more

Pour mettre un lien sur cette page dans le réseau Wicri

{{Explor lien
   |wiki=    Wicri/Lorraine
   |area=    InforLorV4
   |flux=    Main
   |étape=   Exploration
   |type=    RBID
   |clé=     Pascal:08-0215615
   |texte=   A Logical Account of PSPACE
}}

This area was generated with Dilib version V0.6.33.
Data generation: Mon Jun 10 21:56:28 2019. Site generation: Fri Feb 25 15:29:27 2022

	Serveur d'exploration sur la recherche en informatique en Lorraine
	Attention, ce site est en cours de développement ! Attention, site généré par des moyens informatiques à partir de corpus bruts. Les informations ne sont donc pas validées.

Serveur d'exploration sur la recherche en informatique en Lorraine

A Logical Account of PSPACE

A Logical Account of PSPACE

Source :

Descripteurs français

English descriptors

Abstract

Links toward previous steps (curation, corpus...)

Le document en format XML

Pour manipuler ce document sous Unix (Dilib)

Pour mettre un lien sur cette page dans le réseau Wicri